[Imprint][Data Privacy Statement][E-Mail]
Back to main index.
View the specification.
View theorem base summary,
View theorem base listing,
the used properties by spec,
the dependency list,
the symbol table,
data asm specification
aubifs_core
using aubifs-inv,
eraseblock
procedures aubifs_core_format# nat × nat × bool : : node-index × node-index × key-set × key-set × node-store × address-list × bool × error
nondeterministic;
aubifs_core_index_newino# node-index × node-index × key-set × key-set × node-store × address-list × bool : key
nonfunctional
nondeterministic;
aubifs_core_index_contains# key × node-index × node-index × key-set × key-set × node-store × address-list × bool : bool : error
nondeterministic;
aubifs_core_index_lookup# key × node-index × node-index × key-set × key-set × node-store × address-list × bool : bool × node : error
nondeterministic;
aubifs_core_index_store# key × address × node-index × key-set × key-set × node-store × address-list × bool : node-index
nonfunctional
;
aubifs_core_index_remove# key × node-index × key-set × key-set × node-store × address-list × bool : node-index nonfunctional ;
aubifs_core_index_truncate# key × nat × node-index × key-set × key-set × node-store × address-list × bool : node-index
nonfunctional
;
aubifs_core_index_entries# key × node-index × node-index × key-set × key-set × node-store × address-list × bool : stringset : error
nondeterministic;
aubifs_core_journal_get# address × node-index × node-index × key-set × key-set × node-store × address-list × bool : node : error
nondeterministic;
aubifs_core_journal_add1# node × node-index × node-index × key-set × key-set : address × node-store × address-list : bool × error
nondeterministic;
aubifs_core_journal_add2#
node × node × node-index × node-index × key-set × key-set : address × address × node-store × address-list : bool × error
nondeterministic;
aubifs_core_journal_add3#
node × node × node × node-index × node-index × key-set × key-set
: address × address × address × node-store × address-list
: bool × error
nondeterministic;
aubifs_core_journal_add4#
node × node × node × node × node-index × node-index × key-set × key-set
: address × address × address × address × node-store × address-list
: bool × error
nondeterministic;
aubifs_core_journal_add5#
node × node × node × node × node × node-index × node-index × key-set × key-set
: address × address × address × address × address × node-store × address-list
: bool × error
nondeterministic;
aubifs_core_journal_sync# node-index × node-index × key-set × key-set × node-store × address-list : : bool × error
nondeterministic;
aubifs_core_journal_gc# node-index × key-set × key-set : node-index × node-store × address-list : bool nondeterministic;
aubifs_core_gc_copy# : node-index × node-store × address-list nonfunctional nondeterministic;
aubifs_core_gc_drop# node-index × address-list : node-store nonfunctional nondeterministic;
aubifs_core_recover#
bool : address-list × key-set × node-index × key-set × key-set × address-list × node-store : node-index × bool × error
nondeterministic;
aubifs_core_check_commit# node-index × key-set : node-index × key-set × node-store × address-list × bool : error nondeterministic;
aubifs_core_commit# node-index × key-set : node-store × node-index × key-set × address-list : bool × error nondeterministic;
aubifs_core_orphans_contains# key × node-index × node-index × key-set × key-set × node-store × address-list × bool : bool
nonfunctional
;
aubifs_core_orphans_insert# key × node-index × node-index × key-set × node-store × address-list × bool : key-set nonfunctional ;
aubifs_core_orphans_remove# key × node-index × node-index × key-set × node-store × address-list × bool : key-set nonfunctional ;
variables ERR : error flexible;
RO : key-set flexible;
FO : key-set flexible;
RI : node-index flexible;
FI : node-index flexible;
FS : node-store flexible;
LOG : address-list flexible;
VOLSIZE : nat flexible;
KEY : key flexible;
ADR : address flexible;
ND : node flexible;
EXISTS : bool flexible;
N : nat flexible;
SIZE : nat flexible;
NAMES : stringset flexible;
KEY0 : key flexible;
KEY1 : key flexible;
KEY2 : key flexible;
KEY3 : key flexible;
KEY4 : key flexible;
KEY5 : key flexible;
ND0 : node flexible;
ND1 : node flexible;
ND2 : node flexible;
ND3 : node flexible;
ND4 : node flexible;
ND5 : node flexible;
ADR0 : address flexible;
ADR1 : address flexible;
ADR2 : address flexible;
ADR3 : address flexible;
ADR4 : address flexible;
ADR5 : address flexible;
AX : address-list flexible;
AX0 : address-list flexible;
AX1 : address-list flexible;
AS : address-set flexible;
KX : key-list flexible;
KS : key-set flexible;
os : key-set;
CSYNCED : bool flexible;
DOSYNC : bool flexible;
DOSYNC0 : bool flexible;
state variables RI : node-index flexible;
FI : node-index flexible;
RO : key-set flexible;
FO : key-set flexible;
FS : node-store flexible;
LOG : address-list flexible;
CSYNCED : bool flexible;
initialization procedure aubifs_core_format#
if ERR = ESUCCESS
sequential
invariants ri-inj : ⊦ ri-inj(RI);
fi-inj : ⊦ ri-inj(FI);
log-cons : ⊦ log-cons(LOG, FS);
inodekeys-ro : ⊦ RO.inodes?;
inodekeys-fo : ⊦ FO.inodes?;
crash predicate FI = FI` ∧ FO = FO` ∧ FS = FS` ∧ LOG = LOG`
with crash-neutrality
synchronized predicate
CSYNCED
recovery procedure aubifs_core_recover#
if ERR = ESUCCESS
declarations format:
aubifs_core_format#(VOLSIZE, SIZE, DOSYNC; ; RI, FI, RO, FO, FS, LOG, CSYNCED, ERR)
precondition SIZE = LEB_SIZE;
postcondition true;
{if SIZE = LEB_SIZE
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then RI := ∅, FS := ∅, FI := ∅, FO := ∅, RO := ∅, LOG := [], CSYNCED := true
else RI := ?, FS := ?, FI := ?, FO := ?, RO := ?, LOG := ?, CSYNCED := ?}
else abort
}
newino:
aubifs_core_index_newino#(RI, FI, RO, FO, FS, LOG, CSYNCED; KEY)
precondition true;
postcondition true;
{choose n with ¬ inodekey(n) ∈ RI ∧ ¬ inodekey(n) ∈ FO ∧ n ≠ 0 in KEY := inodekey(n)
}
contains:
aubifs_core_index_contains#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS; ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR = ESUCCESS then EXISTS := KEY ∈ RI else EXISTS := ?}
}
lookup:
aubifs_core_index_lookup#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND; ERR)
precondition ri-cons(RI, FS);
postcondition true;
{if ri-cons(RI, FS)
then {fail_or_success#(; ; ERR);
if ERR = ESUCCESS then {EXISTS := KEY ∈ RI; if EXISTS then ND := FS[RI[KEY]] else ND := ?} else EXISTS := ?, ND := ?}
else abort
}
store:
aubifs_core_index_store#(KEY, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI)
precondition ¬ ADR ∈ RI ∧ ADR ∈ FS ∧ key-cons(KEY, FS[ADR]);
postcondition true;
{if ¬ ADR ∈ RI ∧ ADR ∈ FS ∧ key-cons(KEY, FS[ADR]) then RI[KEY] := ADR else abort
}
remove:aubifs_core_index_remove#(KEY, FI, RO, FO, FS, LOG, CSYNCED; RI) precondition true; postcondition true;{RI := RI -- KEY}
truncate:
aubifs_core_index_truncate#(KEY, N, FI, RO, FO, FS, LOG, CSYNCED; RI)
precondition true;
postcondition true;
{let KS = datakeys(KEY, N, RI) in RI := RI \ KS
}
entries:
aubifs_core_index_entries#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; NAMES; ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); if ERR = ESUCCESS then NAMES := dentries(KEY, RI) else NAMES := ?}
}
get:
aubifs_core_journal_get#(ADR, RI, FI, RO, FO, FS, LOG, CSYNCED; ND; ERR)
precondition ADR ∈ FS;
postcondition true;
{if ADR ∈ FS then {ND := FS[ADR], ERR := ESUCCESS or fail#(; ; ERR)} else abort
}
add1:
aubifs_core_journal_add1#(ND1, RI, FI, RO, FO; ADR1, FS, LOG; CSYNCED, ERR)
precondition ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1);
postcondition ri-cons(RI, FS);
{if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1)
then { choose adr1
with new(adr1 ', FS) ∧ ¬ dups(adr1 ')
in {ADR1 := adr1; FS[ADR1] := ND1, LOG := LOG + ADR1, ERR := ESUCCESS}
ifnone ERR := ENOSPC
or {fail#(; ; ERR); ADR1 := ?};
CSYNCED := ?}
else abort
}
add2:
aubifs_core_journal_add2#(ND1, ND2, RI, FI, RO, FO; ADR1, ADR2, FS, LOG; CSYNCED, ERR)
precondition ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2);
postcondition ri-cons(RI, FS);
{if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2)
then { choose adr1, adr2
with new(adr1 ' + adr2 ', FS) ∧ ¬ dups(adr1 ' + adr2 ')
in {ADR1 := adr1, ADR2 := adr2; FS := FS[ADR1, ND1][ADR2, ND2], LOG := (LOG + ADR1) + ADR2, ERR := ESUCCESS}
ifnone ERR := ENOSPC
or {fail#(; ; ERR); ADR1 := ?, ADR2 := ?};
CSYNCED := ?}
else abort
}
add3:
aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR)
precondition ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3);
postcondition ri-cons(RI, FS);
{if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3)
then { choose adr1, adr2, adr3
with new(adr1 ' + (adr2 ' + adr3), FS) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ')
in {ADR1 := adr1, ADR2 := adr2, ADR3 := adr3;
FS := FS[ADR1, ND1][ADR2, ND2][ADR3, ND3], LOG := ((LOG + ADR1) + ADR2) + ADR3, ERR := ESUCCESS}
ifnone ERR := ENOSPC
or {fail#(; ; ERR); ADR1 := ?, ADR2 := ?, ADR3 := ?};
CSYNCED := ?}
else abort
}
add4:
aubifs_core_journal_add4#(ND1, ND2, ND3, ND4, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, FS, LOG; CSYNCED, ERR)
precondition ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3) ∧ node-cons(ND4.key, ND4)
;
postcondition ri-cons(RI, FS);
{if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3) ∧ node-cons(ND4.key, ND4)
then { choose adr1, adr2, adr3, adr4
with new(adr1 ' + adr2 ' + (adr3 ' + adr4), FS) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ' + adr4 ')
in {ADR1 := adr1, ADR2 := adr2, ADR3 := adr3, ADR4 := adr4;
FS := FS[ADR1, ND1][ADR2, ND2][ADR3, ND3][ADR4, ND4], LOG := (((LOG + ADR1) + ADR2) + ADR3) + ADR4, ERR := ESUCCESS}
ifnone ERR := ENOSPC
or {fail#(; ; ERR); ADR1 := ?, ADR2 := ?, ADR3 := ?, ADR4 := ?};
CSYNCED := ?}
else abort
}
add5:
aubifs_core_journal_add5#(ND1, ND2, ND3, ND4, ND5, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, ADR5, FS, LOG; CSYNCED, ERR)
precondition ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3)
∧ node-cons(ND4.key, ND4) ∧ node-cons(ND5.key, ND5)
;
postcondition ri-cons(RI, FS);
{if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3) ∧ node-cons(ND4.key, ND4)
∧ node-cons(ND5.key, ND5)
then { choose adr1, adr2, adr3, adr4, adr5
with new(adr1 ' + adr2 ' + adr3 ' + (adr4 ' + adr5), FS) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ' + adr4 ' + adr5 ')
in {ADR1 := adr1, ADR2 := adr2, ADR3 := adr3, ADR4 := adr4, ADR5 := adr5;
FS := FS[ADR1, ND1][ADR2, ND2][ADR3, ND3][ADR4, ND4][ADR5, ND5], LOG := ((((LOG + ADR1) + ADR2) + ADR3) + ADR4) + ADR5,
ERR := ESUCCESS}
ifnone ERR := ENOSPC
or {fail#(; ; ERR); ADR1 := ?, ADR2 := ?, ADR3 := ?, ADR4 := ?, ADR5 := ?};
CSYNCED := ?}
else abort
}
sync:
aubifs_core_journal_sync#(RI, FI, RO, FO, FS, LOG; ; CSYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR); CSYNCED := ERR = ESUCCESS}
}
gc:
aubifs_core_journal_gc#(FI, RO, FO; RI, FS, LOG; CSYNCED)
precondition ri-cons(RI, FS);
postcondition ri-cons(RI, FS);
{if ri-cons(RI, FS) then {aubifs_core_gc_copy#(; RI, FS, LOG); aubifs_core_gc_drop#(RI, LOG; FS); CSYNCED := ?} else abort
}
gc-step
: aubifs_core_gc_copy#(; RI, FS, LOG)
{choose KX, AX
with ¬ dups(KX) ∧ ¬ dups(AX) ∧ new(AX, FS) ∧ KX.toSet ⊆ dom RI ∧ # KX = # AX ∧ AX.toSet ∩ LOG.toSet = ∅
in {FS[AX] := FS[RI[KX]], LOG := LOG + AX; RI[KX] := AX}
}
;
gc-drop : aubifs_core_gc_drop#(RI, LOG; FS){choose AS with AS ∩ range RI = ∅ ∧ LOG.toSet ∩ AS = ∅ in FS := FS \ AS};
recover:
aubifs_core_recover#(DOSYNC; AX, KS, FI, RO, FO, LOG, FS; RI, CSYNCED, ERR)
precondition true;
postcondition true;
{{fail_or_success#(; ; ERR);
if ERR = ESUCCESS
then {RI := FI, RO := FO, AX := LOG; KS := RO; CSYNCED := true}
else RI := ?, FI := ?, FS := ?, LOG := ?, RO := ?, FO := ?, AX := ?, KS := ?, CSYNCED := ?}
}
check-commit:
aubifs_core_check_commit#(RI, RO; FI, FO, FS, LOG, CSYNCED; ERR)
precondition ri-cons(RI, FS);
postcondition true;
{if ri-cons(RI, FS) then {aubifs_core_commit#(RI, RO; FS, FI, FO, LOG; CSYNCED, ERR) or ERR := ESUCCESS} else abort
}
commit:
aubifs_core_commit#(RI, RO; FS, FI, FO, LOG; CSYNCED, ERR)
precondition ri-cons(RI, FS);
postcondition true;
{if ri-cons(RI, FS)
then { {choose AS with AS ∩ range RI = ∅ in FI := RI, FO := RO, FS := FS \ AS, LOG := [], ERR := ESUCCESS; CSYNCED := true}
or {fail#(; ; ERR); CSYNCED := ?}}
else abort
}
orphans-contains:
aubifs_core_orphans_contains#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS)
precondition KEY.inode?;
postcondition true;
{if KEY.inode? then EXISTS := KEY ∈ RO else abort
}
orphans-insert:
aubifs_core_orphans_insert#(KEY, RI, FI, FO, FS, LOG, CSYNCED; RO)
precondition KEY.inode?;
postcondition true;
{if KEY.inode? then RO := RO ++ KEY else abort
}
orphans-remove:
aubifs_core_orphans_remove#(KEY, RI, FI, FO, FS, LOG, CSYNCED; RO)
precondition KEY.inode?;
postcondition true;
{if KEY.inode? then RO := RO -- KEY else abort
}
end data asm specification